SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Hilbert's program</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Hilbert's program</span></span>

</h1>

</header>

/* start https://en.wikipedia.org/ */

.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style>

<p>In <a href="Mathematics" title="Mathematics">mathematics</a>, <b>Hilbert's program</b>, formulated by <a href="Germans" title="Germans">German</a> mathematician <a href="David_Hilbert" title="David Hilbert">David Hilbert</a> in the early 1920s,<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> was a proposed solution to the <a href="Foundational_crisis_of_mathematics" class="mw-redirect" title="Foundational crisis of mathematics">foundational crisis of mathematics</a>, when early attempts to clarify the <a href="Foundations_of_mathematics" title="Foundations of mathematics">foundations of mathematics</a> were found to suffer from paradoxes and inconsistencies. As a solution, Hilbert proposed to ground all existing theories to a finite, <a href="Completeness_(logic)" title="Completeness (logic)">complete</a> set of <a href="Axiom" title="Axiom">axioms</a>, and provide a proof that these axioms were <a href="Consistent" class="mw-redirect" title="Consistent">consistent</a>. Hilbert proposed that the consistency of more complicated systems, such as <a href="Real_analysis" title="Real analysis">real analysis</a>, could be proven in terms of simpler systems. Ultimately, the consistency of all of mathematics could be reduced to basic <a href="Arithmetic" title="Arithmetic">arithmetic</a>.

</p><p><a href="G%C3%B6del's_incompleteness_theorems" title="Gödel's incompleteness theorems">Gödel's incompleteness theorems</a>, published in 1931, showed that Hilbert's program was unattainable for key areas of mathematics. In his first theorem, Gödel showed that any consistent system with a <a href="Computable" class="mw-redirect" title="Computable">computable</a> set of axioms which is capable of expressing arithmetic can never be complete: it is possible to construct a statement that can be shown to be true, but that cannot be derived from the formal rules of the system. In his second theorem, he showed that such a system could not prove its own consistency, so it certainly cannot be used to prove the consistency of anything stronger with certainty. This refuted Hilbert's assumption that a finitistic system could be used to prove the consistency of itself, and therefore could not prove everything else.

</p>

<div class="mw-heading mw-heading2"><h2 id="Statement_of_Hilbert's_program">Statement of Hilbert's program</h2></div>

<p>The main goal of Hilbert's program was to provide secure foundations for all mathematics. In particular, this should include:

</p>

<ul><li>A formulation of all mathematics; in other words all mathematical statements should be written in a precise <a href="Formal_language" title="Formal language">formal language</a>, and manipulated according to well defined rules.</li>

<li>Completeness: a proof that all true mathematical statements can be proved in the formalism.</li>

<li>Consistency: a proof that no contradiction can be obtained in the formalism of mathematics. This consistency proof should preferably use only "finitistic" reasoning about finite mathematical objects.</li>

<li>Conservation: a proof that any result about "real objects" obtained using reasoning about "ideal objects" (such as <a href="Uncountable" class="mw-redirect" title="Uncountable">uncountable</a> sets) can be proved without using ideal objects.</li>

<li><a href="Decidability_(logic)" title="Decidability (logic)">Decidability</a>: there should be an algorithm for deciding the truth or falsity of any mathematical statement.</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Gödel's_incompleteness_theorems">Gödel's incompleteness theorems</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div role="note" class="hatnote navigation-not-searchable">Main article: <a href="G%C3%B6del's_incompleteness_theorems" title="Gödel's incompleteness theorems">Gödel's incompleteness theorems</a></div>

<p><a href="Kurt_G%C3%B6del" title="Kurt Gödel">Kurt Gödel</a> showed that most of the goals of Hilbert's program were impossible to achieve, at least if interpreted in the most obvious way. Gödel's second incompleteness theorem shows that any consistent theory powerful enough to encode addition and multiplication of integers cannot prove its own consistency. This presents a challenge to Hilbert's program:

</p>

<ul><li>It is not possible to formalize <b>all</b> mathematical true statements within a formal system, as any attempt at such a formalism will omit some true mathematical statements. There is no complete, consistent extension of even <a href="Peano_axioms" title="Peano axioms">Peano arithmetic</a> based on a <a href="Computably_enumerable" class="mw-redirect" title="Computably enumerable">computably enumerable</a> set of axioms.</li>

<li>A theory such as Peano arithmetic cannot even prove its own consistency, so a restricted "finitistic" subset of it certainly cannot prove the consistency of more powerful theories such as set theory.</li>

<li>There is no algorithm to decide the truth (or provability) of statements in any consistent extension of Peano arithmetic. Strictly speaking, this negative solution to the <a href="Entscheidungsproblem" title="Entscheidungsproblem">Entscheidungsproblem</a> appeared a few years after Gödel's theorem, because at the time the notion of an algorithm had not been precisely defined.</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Hilbert's_program_after_Gödel">Hilbert's program after Gödel</h2></div>

<p>Many current lines of research in <a href="Mathematical_logic" title="Mathematical logic">mathematical logic</a>, such as <a href="Proof_theory" title="Proof theory">proof theory</a> and <a href="Reverse_mathematics" title="Reverse mathematics">reverse mathematics</a>, can be viewed as natural continuations of Hilbert's original program. Much of it can be salvaged by changing its goals slightly (Zach 2005), and with the following modifications some of it was successfully completed:

</p>

<ul><li>Although it is not possible to formalize <b>all</b> mathematics, it is possible to formalize essentially all the mathematics that anyone uses. In particular <a href="Zermelo%E2%80%93Fraenkel_set_theory" title="Zermelo–Fraenkel set theory">Zermelo–Fraenkel set theory</a>, combined with <a href="First-order_logic" title="First-order logic">first-order logic</a>, gives a satisfactory and generally accepted formalism for almost all current mathematics.</li>

<li>Although it is not possible to prove completeness for systems that can express at least the Peano arithmetic (or, more generally, that have a computable set of axioms), it is possible to prove forms of completeness for many other interesting systems. An example of a non-trivial theory for which <a href="Complete_theory" title="Complete theory">completeness</a> has been proved is the theory of <a href="Algebraically_closed_field" title="Algebraically closed field">algebraically closed fields</a> of given <a href="Characteristic_(algebra)" title="Characteristic (algebra)">characteristic</a>.</li>

<li>The question of whether there are finitary consistency proofs of strong theories is difficult to answer, mainly because there is no generally accepted definition of a "finitary proof". Most mathematicians in proof theory seem to regard finitary mathematics as being contained in Peano arithmetic, and in this case it is not possible to give finitary proofs of reasonably strong theories. On the other hand, Gödel himself suggested the possibility of giving finitary consistency proofs using finitary methods that cannot be formalized in Peano arithmetic, so he seems to have had a more liberal view of what finitary methods might be allowed. A few years later, <a href="Gerhard_Gentzen" title="Gerhard Gentzen">Gentzen</a> gave a <a href="Gentzen's_consistency_proof" title="Gentzen's consistency proof">consistency proof</a> for Peano arithmetic. The only part of this proof that was not clearly finitary was a certain <a href="Transfinite_induction" title="Transfinite induction">transfinite induction</a> up to the <a href="Ordinal_number" title="Ordinal number">ordinal</a> <a href="Epsilon_number" title="Epsilon number">ε<sub>0</sub></a>. If this transfinite induction is accepted as a finitary method, then one can assert that there is a finitary proof of the consistency of Peano arithmetic. More powerful subsets of <a href="Second-order_arithmetic" title="Second-order arithmetic">second-order arithmetic</a> have been given consistency proofs by <a href="Gaisi_Takeuti" title="Gaisi Takeuti">Gaisi Takeuti</a> and others, and one can again debate about exactly how finitary or constructive these proofs are. (The theories that have been proved consistent by these methods are quite strong, and include most "ordinary" mathematics.)</li>

<li>Although there is no algorithm for deciding the truth of statements in Peano arithmetic, there are many interesting and non-trivial theories for which such algorithms have been found. For example, <a href="Alfred_Tarski" title="Alfred Tarski"> Tarski</a> found an algorithm that can decide the truth of any statement in <a href="Analytic_geometry" title="Analytic geometry">analytic geometry</a> (more precisely, he proved that the theory of <a href="Real_closed_field" title="Real closed field">real closed fields</a> is decidable). Given the <a href="Cantor%E2%80%93Dedekind_axiom" title="Cantor–Dedekind axiom">Cantor–Dedekind axiom</a>, this algorithm can be regarded as an algorithm to decide the truth of any statement in <a href="Euclidean_geometry" title="Euclidean geometry">Euclidean geometry</a>. This is substantial as few people would consider Euclidean geometry a trivial theory.</li></ul>

<ul><li><a href="Grundlagen_der_Mathematik" title="Grundlagen der Mathematik">Grundlagen der Mathematik</a></li>

<li><a href="Foundational_crisis_of_mathematics" class="mw-redirect" title="Foundational crisis of mathematics">Foundational crisis of mathematics</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFZach2023" class="citation cs2">Zach, Richard (2023), Zalta, Edward N.; Nodelman, Uri (eds.), <a rel="nofollow" class="external text" href="https://plato.stanford.edu/archives/spr2023/entries/hilbert-program/">"Hilbert's Program"</a>, <i>The Stanford Encyclopedia of Philosophy</i> (Spring 2023 ed.), Metaphysics Research Lab, Stanford University<span class="reference-accessdate">, retrieved <span class="nowrap">2023-07-05</span></span></cite></span>

</li>

</ol></div></div>

<ul><li>G. Gentzen, 1936/1969. Die Widerspruchfreiheit der reinen Zahlentheorie. <i><a href="Mathematische_Annalen" title="Mathematische Annalen">Mathematische Annalen</a></i> 112:493–565. Translated as 'The consistency of arithmetic', in <i>The collected papers of Gerhard Gentzen</i>, M. E. Szabo (ed.), 1969.</li>

<li>D. Hilbert. 'Die Grundlegung der elementaren Zahlenlehre'. <i>Mathematische Annalen</i> 104:485–94. Translated by W. Ewald as 'The Grounding of Elementary Number Theory', pp. 266–273 in Mancosu (ed., 1998) <i>From Brouwer to Hilbert: The debate on the foundations of mathematics in the 1920s</i>, Oxford University Press. New York.</li>

<li><a href="Steve_Simpson_(mathematician)" title="Steve Simpson (mathematician)">S.G. Simpson</a>, 1988. <a rel="nofollow" class="external text" href="https://www.personal.psu.edu/t20/papers/hilbert-jsl-1988.pdf">Partial realizations of Hilbert's program (pdf)</a>. <i><a href="Journal_of_Symbolic_Logic" title="Journal of Symbolic Logic">Journal of Symbolic Logic</a></i> 53:349–363.</li>

<li><a href="Richard_Zach" title="Richard Zach">R. Zach</a>, 2006. Hilbert's Program Then and Now. <i>Philosophy of Logic</i> 5:411–447, <a rel="nofollow" class="external text" href="https://arxiv.org/abs/math/0508572">arXiv:math/0508572</a> [math.LO].</li></ul>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><cite id="CITEREFRichard_Zach" class="citation encyclopaedia cs1">Richard Zach. <a rel="nofollow" class="external text" href="https://plato.stanford.edu/entries/hilbert-program/">"Hilbert's Program"</a>. In <a href="Edward_N._Zalta" title="Edward N. Zalta">Zalta, Edward N.</a> (ed.). <i><a href="Stanford_Encyclopedia_of_Philosophy" title="Stanford Encyclopedia of Philosophy">Stanford Encyclopedia of Philosophy</a></i>.</cite></li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox authority-control" aria-label="Navbox390" style="padding:3px"><table class="nowraplinks hlist navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Authority control databases: National </th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"><ul><li><span class="uid"><a rel="nofollow" class="external text" href="https://d-nb.info/gnd/4209255-3">Germany</a></span></li></ul></div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2024-08-18" href="https://en.wikipedia.org/wiki/?title=Hilbert's_program&oldid=1240954687">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>